T:Type, L:T List, P:(TTProp), u:T. (x<yu.L.P(x,y))  (yL. P(u,y)) & (x<yL.P(x,y)) 

latex

Definitions	P  Q, x:A. B(x), x before y  l, x:A. B(x), (x  l), P & Q, P  Q, t  T, Prop, {T}, True, x(s1,s2), P  Q, P  Q, x. t(x), (x<yL.P(x;y)), xL. P(x), SQType(T)
Lemmas	iff functionality wrt iff, all functionality wrt iff, implies functionality wrt iff, cons before, iff wf, l before wf, l member wf